Section: Software

The Alea library for randomized algorithms

Participants : Christine Paulin-Mohring [contact] , David Baelde.

Criteria for Software Self-Assessment: A-2, SO-3, SM-2, EM-3, SDL-4, OC-4.

The ALEA library is a Coq development for modeling randomized functional programs as distributions using a monadic transformation. It contains an axiomatisation of the real interval $[0,1]$ and its extension to positive real numbers. It introduces definition of distributions and general rules for approximating the probability that a program satisfies a given property.

It is distributed as open source, at http://www.lri.fr/~paulin/ALEA . It is currently used as a basis of the Certicrypt environment (MSR-INRIA joint research center, Imdea Madrid, INRIA Sophia-Antipolis) for formal proofs for computational cryptography  [53] . It is also experimented in LABRI as a basis to study formal proofs of probabilistic distributed algorithms.